Trait isotope::ctx::subst::SubstCtx [−][src]
pub trait SubstCtx { type Ctx: TyCtxMut; fn subst_var(
&mut self,
ix: u32,
annot: Option<&TermId>
) -> Result<Option<TermId>, Error>; fn push_param(
&mut self,
param_ty: Option<&TermId>
) -> Result<Option<TermId>, Error>; fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool; fn ctx(&mut self) -> &mut Self::Ctx; fn pop_param(&mut self) -> Result<(), Error>; fn is_var_null(&self) -> bool; fn cache(
&mut self,
_term: &TermId,
_subst: Option<&TermId>
) -> Result<(), Error> { ... } fn try_subst(
&mut self,
_term: &Term
) -> Option<Result<Option<TermId>, Error>> { ... } fn subst_constrain(
&mut self,
ix: u32,
annot: Option<&TermId>
) -> Result<Option<TermId>, Error> { ... } fn cons_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::ConsCtx { ... } fn eq_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::TermEqCtx { ... } fn push_param_ctx(&mut self, param_ty: Option<&TermId>) -> Result<(), Error> { ... } }
Expand description
A context for substituting terms
Associated Types
Required methods
Substutite a variable, with an optional un-substituted annotation. Does not add the annotation as a constraint.
Returns an error if the annotation gives a type error. Implementations may return an error when provided a null annotation, or may perform a substitution with no constraint.
Push a parameter onto this context with an optional annotation, returning the annotation substitution, if any
Check whether this context can potentially make any changes to a term with the given filter
fn is_var_null(&self) -> bool
[src]
fn is_var_null(&self) -> bool
[src]Whether no variables are substituted by this context
Provided methods
Cache a substitution result. May cause erroneous behaviour if the result passed is invalid!
May return an error on invalid input, though this is not guaranteed.
Attempt to substitute an entire term. Return None
if substitution should proceed recursively instead.
Substutite a variable, with an optional un-substituted annotation, adding the annotation as a constraint.
Returns an error if the annotation gives a type error. Implementations may return an error when provided a null annotation, or may perform a substitution with no constraint.
Get the underlying consing context
Get the underlying equality context